A, B, C:MsgA. A || B  C || A  C || B  C || A  B 

latex

Definitions

MsgA, t  T, x:A. B(x), M1 || M2, M1  M2, P  Q, P & Q, x. t(x), Id, Knd, type List, IdLnk, x.A(x), x:A  B(x), product-deq(A;B;a;b), x:AB(x), Top, a:A fp B(a), State(ds), Type, t.1, f(x)?z, rcv(l,tg), Void, IdDeq, f  g, KindDeq, Valtype(da;k), t.2, IdLnkDeq, , , f || g, M1 ||decl M2, mk-ma, S  T, suptype(S; T), f(x), s = t, , b, <a, b>, False, A, left + right, P  Q, b, x  dom(f), P  Q, Unit, if b then t else f fi , x:A.B(x), {T}

Lemmas

subtype-fpf-cap-top, ma-state-subtype, fpf-compatible-triple, top wf, fpf-join-dom2, fpf-join-ap-sq, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, bnot wf, not wf, assert wf, fpf-ap wf, subtype-fpf-cap-void, id-deq wf, Id wf, Kind-deq wf, Knd wf, bool wf, rationals wf, IdLnk wf, idlnk-deq wf, ma-state wf, ma-valtype wf, fpf-join wf, pi1 wf, fpf-cap wf, rcv wf, pi2 wf, fpf-trivial-subtype-top, product-deq wf, fpf-compatible-join, ma-compatible wf, msga wf